es:ES, e, e':E. (e <loc e')  [e, e'] = ([e, pred(e')] @ [e'])  E List 

latex

Definitions	E, as @ bs, filter(P;l), t  T, x:A. B(x), P & Q, P  Q, P  Q, pred(e), 1of(t), before(e), es-ble{i:l}(es;e;e'), , [e, e'], ES, (e <loc e'), b, A, b, Prop, first(e), Unit, False, True, T, true, P  Q, x(s), x. t(x), xL. P(x), P  Q, e  e'
Lemmas	assert-es-ble, filter trivial, l all reduce, assert of band, btrue wf, squash wf, true wf, append wf, filter wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-first wf, bool wf, bnot wf, not wf, assert wf, es-locl wf, event system wf, filter append, es-ble wf, es-before wf, es-pred wf, es-locl-iff, es-E wf